Step of Proof: inv_image_ind_tp 12,41
Inference at * 1 1 1 1 
Iof proof for Lemma inv image ind tp:



1. T : Type
2. r : TT
3. S : Type
4. f : ST
5. WellFnd{i}(T;x,y.r(x,y))
6. P : S
7. j:S. (k:S. r(f(k),f(j))  P(k))  P(j)
8. n : S
  P(n) 
latex
 by (%S% 
\p.let x = get_distinct_var `x' p 
\p.in let n = get_var_arg `n` p 

\p.inin let S = get_term_arg `S` p 
\p.in let T = get_term_arg `T` p 

\p.inin let f = get_term_arg `f` p 
\p.in 
\p.Assert 
\p.As(mk_all_term x T 
\p.As(m(mk_all_term n S

\p.As(m(m(mk_implies_term 
\p.As(m(m(mk(mk_equal_term T (mk_apply_term f (mvt n)) (mvt x)) 

\p.As(m(m(mk(m(concl p)))) p) 
latex

\p1: .....assertion..... NILNIL

\p1:   x:T, n:S. (f(n) = x)  P(n)
\p2: 

\p2: 9. x:T, n:S. (f(n) = x)  P(n)
\p2:   P(n)
\p.

origin